es:ES, a:Atom1, e:E.
loc(e) || a
 ((((first(e)))
 (( ((isrcv(pred(e)))  val(pred(e)):valtype(pred(e))||a)
 (( es_state_when(es;pred(e)):es_state(es;loc(pred(e)))||a
 (( es_state_when(es;e):es_state(es;loc(e))||a)
 & (((isrcv(e))  val(e):valtype(e)||a)
 & ( es_state_when(es;e):es_state(es;loc(e))||a
 & ( e sends || a)) 

latex

Definitions	x when e, (state when e), t  T, A, P & Q, P  Q, x:A. B(x), , A c B, i || a, s(now)
Lemmas	es-read-state wf, event system wf, es-E wf, es-atom wf, false wf, es-first wf, es-val wf, es-valtype wf, es-isrcv wf, assert wf, es state when wf, es-pred wf, es-loc wf, es state wf, free-from-atom wf1, es-choose wf, es-send wf, Id wf, es-trans wf, implies-es-atom-axiom, es-machine-axiom